\chapter{Extending FGJ with JavaPict}
JavaPict can be proved to be type safe by extending FGJ to include the defining functions of JavaPict i.e choice and parallel. Since we have not implemented replication we need not bother about it. FGJ has a compact syntax which is helpful in making us concentrate on the newly added features and prove type safety.
FGJ is extended by adding two new expressions, one for choice and other one for parallel. Lets call this extension Featherweight Generic JavaPict(FGJP).

\section{Introduction}
Generic Java adds generic types to Java. The following example shows two ways of declaring generic type. One is in the class declaration and other in the method declaration. Thus in the code below, X and Y are the generic types declared in class while Z is declared in method setfirst. 
\begin{verbatim}
    class Key extends Object{
        Key(){super();}
    }

    class Value extends Object{
        Value(){super();}
    }

    class Pair<X extends Object, Y extends Object> 
                                     extends Object{
        X first;
        Y second;
        Pair(X first, Y second){
            super();
            this.first = first; 
            this.second = second;
        }
        <Z extends Object> Pair<Z, Y> setfirst(Z newfirst){
            return new Pair<Z, Y>(newfirst, this.second);
        }
    }
\end{verbatim}
Generic types can be implemented in two styles. They may be implemented by using method of type-passing, wherein the runtime system carries information about type parameters. Or they may be implemented by using type erasure. Java employs the method of type erasure. We will use the first method which involves direct semantics which maintains the information at runtime. \cite{FGJ} have shown the correspondence between the two implementation styles. 
Type erasure involves replacing a type variable with its bound. Bound of a type is discussed in the next section in detail. The above code after erasure will look as follows:
\begin{verbatim}
    class Key extends Object{
        Key(){super();}
    }

    class Value extends Object{
        Value(){super();}
    }

    class Pair<Object, Object> 
                       extends Object{
        Object first;
        Object second;
        Pair(Object first, Object second){
            super();
            this.first = first; 
            this.second = second;
        }
        Pair setfirst(Object newfirst){
            return new Pair(newfirst, this.second);
        }
    }
\end{verbatim}
All occurrences of type variables X, Y and Z are replaced by their bounds, Object in this case. The field selection expression\\
\begin{verbatim}
       new Pair<Key, Value>(new Key(), new Value()).second;
\end{verbatim}
erases to\\
\begin{verbatim}
       (B)mew Pair(new Key(), new Value()).second;
\end{verbatim}
The downcast is added to recover type information which is lost due to erasure. Such downcasts are call $synthetic$. Erasure method enjoys the property of cast-iron guarantee, which proves that if a FGJ program is well-typed then no downcast inserted by the erasure transformation will fail at runtime.
\section{Syntax}

\begin{table}
\begin{tabular}{|p{\linewidth}|}
    \hline
    {\bf Syntax} \\ \\
    $\tau$ = T $|$ void \\
    \\
    T := X$|$N \\ \\
    N := C$<{\overline T}>$ \\ \\
    L := class C$<{\overline X}\triangleleft{\overline N}>$ $\triangleleft$ N
    \{${\overline T}$ ${\overline f}$; K ${\overline M}$\} \\ \\
    K := C(${\overline T}$ ${\overline f}$) \{ super(${\overline f}$);
    this.${\overline f}$ = ${\overline f}$;\}\\ \\
    M := $<{\overline X}$ $\triangleleft$ ${\overline N}>$ $\tau$ m(${\overline T}$
    ${\overline x}$)\{ return e; \}\\ \\
    e := x $|$ e.f $|$ e.m$<{\overline T}>$(${\overline e}$) $|$ new N(${\overline
    e}$) $|$ (N)e $|$ e$_1$.run() $\vee$ e$_2$.run() $|$  \\
	\hspace{1cm}e$_1$.run() $\|$ e$_2$.run() \\ \\
    \hline
\end{tabular}
\caption{Syntax for FGJP}
\end{table}

As seen in the previous discussion of JavaPict, choice and parallel are operations that can be applied on an object of class Process. Also recall that choice necessarily means choosing between two processes $p_1$ and $p_2$ and deciding whether p$_1$.run() will proceed or p$_2$.run(). Similarly, parallel means running $p_1$.run() and $p_2$.run() in parallel or simultaneously. The method run() returns nothing. This can be captured by introducing the type $void$ in the syntax.   We also assume the basic syntax to include a class Process which has a method named run, which takes no arguments and returns a void. \\
The syntax for FGJP is shown in table 6.1. void is a primitive type in Java. Similar to the notation described earlier, X, Y and  Z will denote type variables. T, U, V will denote
types, and N, M, P, or Q are the actual types, also $\tau$ will denote type along with the new type void. K is reserved for constructor and M for method declaration. \\
The method return type could be a type, or a variable type or void. 
The $\pi$ calculus functions for choosing a process and for running two processes in
parallel are the new expressions that are added to FGJ. Choice operation i.e.
e$_1$.run() $\vee$ e$_2$.run() and parallel operation e$_1$.run() $\|$
e$_2$.run() where e$_1$ and e$_2$ are of type process. The typing restriction is discussed in later sections of this chapter. A class C is a process if it itself extends the base class Process or it extends a class D which is a process. Other expressions include variable access, field access, method call, a new object creation and casting an expression.\\

The symbol $\triangleleft$ is used as keyword for extends. Thus C extends D is written as C $\triangleleft$	 D. Also $<$: is
used to denote subclass relation. Thus C is a subclass of D is written as C $<$:
D. The reflexive and transitive closure of subclass relation is denoted by $\unlhd$ as shown in Table 6.2.
\section{Auxiliary Functions}
\begin{table}[htb!]
\begin{tabular}{|p{\linewidth}|}
    \hline
    {\bf Subclass}\\
    \begin{center}
    \begin{tabular}{ccc}
    C $\unlhd$ C & $\frac {C\ \unlhd\ D\ \  D\ \unlhd\ E}{C\ \unlhd\ E}$ &  $\frac
    {class\ C<\overline X\ \triangleleft\ \overline N>\ \triangleleft\ 
    D<\overline{T}>\ \{ ... \}} {C\ \unlhd\ D}$
    \end{tabular}
    \end{center} \\
    \hline
    {\bf Fields}\\
    \begin{center}
    \begin{tabular}{p{0.8\linewidth}r}
    `	fields(Object) := $\bullet$ & F-OBJECT\\  
	    &\hspace{10cm}\\
	    {\large $\frac {class\ C<\overline X\ \triangleleft\ \overline N>\ 
	    \triangleleft\  N \{\  \overline T \ \overline f;\ K \ \overline M\}}
	    {fields(C)\ =\ \overline U \ \overline g, \ [\overline{T}/\overline{X}]\overline{S} \ \overline{f}}$} \hspace{10cm}& F-CLASS
    \end{tabular}
    \end{center}\\\\
    \hline
    {\bf Method functions}
    \begin{center}
    \begin{tabular}{lr}
      $\dfrac 
	{
	  \splitfrac{class\ C<\overline X \triangleleft \overline N>\ \triangleleft\
      N \{\  \overline T \ \overline f;\ K \ \overline M\}} 
		    {<\overline X\ \triangleleft\ \overline N>\ \tau\ m(\overline T\
      \overline x)\{\ return\ e;\ \} \ \ m \in \overline M}
	}
	{mtype(m,\ C<\overline{T}>)\ =\ [\overline{T}/\overline{X}](<\overline{X}\triangleleft \overline N> \rightarrow \tau)}$ \hspace{2cm} & MT-CLASS \\
      &\\
      &\\
      $\dfrac 
	{
	  \splitfrac{class\ C<\overline X\ \triangleleft\ \overline N>\ \triangleleft\
      N \{\  \overline T \ \overline f;\ K \ \overline M\}} 
		    {<\overline X\ \triangleleft\ \overline N>\ \tau\ m(\overline T\
      \overline x)\{\ return\ e;\ \} \ \ m \notin \overline M}
	}
	{mtype(m,\ C<\overline{T}>)\ =\ mtype(m,\ [\overline{T}/\overline{X}]N)}$ & MT-SUPER 
    \end{tabular}
    \end{center}\\\\
    \hline
    {\bf Process functions}
    \begin{center}
    \begin{tabular}{lr}
      $\dfrac
      {\splitfrac{class\ C<\overline X \triangleleft \overline N>\ \triangleleft\  N
      \{\  \overline T \ \overline f;\ K \ \overline M\}}{\splitfrac{\Gamma;\ \Delta \
      \vdash C <: Process}{ <\overline{Y} \ \triangleleft \ \overline{P}>\ void\ run
      (\overline{G} \ \overline{f})\ \{\ return\ e;\ \}\ \in\ M}\ }}
      {isProcess(new\ C<\overline{T}>)\ =\ true}$ \hspace{1cm} & F-PROCESS  
    \end{tabular}
    \end{center}\\
    \hline
\end{tabular}
\caption{Auxiliary functions}
\end{table}
Some helper functions are defined as shown in table 6.2 to make the proof more understandable and modular. If C is a class then fields(C) gives the  sequence of fields and
corresponding types that are defined in the class definition C. The function $mtype$ returns the type
the method i.e the parameter type as well as the return type. The method $mbody$ gives the parameters 
and the return value. The function isProcess() is a boolean function which takes a class as parameter and returns true if the given class is a subclass of Process.

\section{Subtyping and Well-formedness}
\begin{table}
  \begin{tabular}{|p{\linewidth}|}
    \hline	
    {\bf Bound of type}\\
    \begin{tabular}{p{0.5\linewidth}r}
    bound$_{\bigtriangleup}$(x) = $\bigtriangleup$(x) & bound$_{\bigtriangleup}$(N) = N 
    \end{tabular}\\
    \hline
    {\bf Subtyping} 
    \\
    \begin{tabular}{p{0.8\linewidth}r}
    $\Delta \ \vdash \ \tau \ \prec:\ \tau$ \hspace{10cm}& S-REFL\\
    &\\
    $\Delta \ \vdash \ $void $ \nprec $ T & S-VOIDSUB\\
    &\\
    $\Delta \ \vdash \ $ T $ \nprec $ void & S-VOIDSUP \\
    &\\
    \large{$\frac{\Delta\ \vdash \ S \prec: T \ \ \ \ \Delta\ \vdash \ T \prec: U}{\Delta\ \vdash \ S \prec: U}$} & S-TRANS\\
    &\\
    $\Delta \ \vdash X \prec: \ \Delta(X)$ & S-VAR \\
    & \\
    \large{$\frac{class \ C<\overline{X}\triangleleft\overline{N}>\triangleleft N \{ ...\}}{\Delta \ \vdash C<\overline{T}>\prec: \ [T/X]N}$} & S-CLASS
    \end{tabular}\\
    \\
    \hline
    {\bf Well-formed types}\\ 
    \begin{tabular}{p{0.8\linewidth}l}
    $\Delta \ \vdash$ void ok & WF-VOID \\
    &\\
    $\Delta \ \vdash$ Object ok & WF-OBJECT \\
    &\\
    \large{$\frac{X\ \in  \ dom(\Delta)}{\Delta \ \vdash \ X \ ok}$} & WF-VAR \\
    &\\
    $\frac{\splitfrac{class\ C<\overline{X}\triangleleft\overline{N}>\triangleleft\ N \ \{ ...\}}{\Delta \ \vdash \ \overline{T} \ ok \ \ \ \ \  \ \Delta \ \vdash \ \overline{T} \prec: \ [\overline{T}/\overline{X}]N}}{\Delta \ \vdash \ C<\overline{T}> \ ok}$  & WF-CLASS \\
    &\\
    $\frac{\splitfrac{\Delta;\Gamma \ \vdash \ e_1 \ ok \ \ \ \Delta; \Gamma \ \vdash \ e_2 \ ok}{isProcess(e_1) = true \ \ \ isProcess(e_2) = true}}{\splitfrac{\Delta; \Gamma \ \vdash \ choose(e_1,\ 	 e_2) \ ok}{\Delta; \Gamma \ \vdash \ parallel(e_1,\ e_2) \ ok}}$
    \end{tabular}\\
  \\
    \hline 
    {\bf Valid downcast} \\
    \\
    \begin{tabular}{p{0.8\linewidth}r}
    $\frac{dcast(C,\ D)\ \ \ \ \ \ dcast(D,\ E)}{dcast(C,\ E)}$ & VD-TRANS \\
    &\\
    $\frac{\splitfrac{class\ C<\overline{X}\triangleleft\overline{N}>\triangleleft\ D<\overline{T}> \ \{ ...\}}{\overline{X} = FV(\overline{T})\hspace{4cm} }}{dcast(C, \ D)}$ & VD-DCAST \\
    FV($\overline{T}$) denotes the set of type variables in $\overline{T}$. & 
    \end{tabular}\\ \\
    \hline 
    {\bf Valid method overriding}\\
    \\
    $\frac{\splitfrac{mtype(m, \ N)\ =\ <\overline{Z}\triangleleft \overline{Q}> \ \overline{U} \rightarrow \ U_o \ implies \ \overline{P}, \ \overline{T} \ = \ [\overline{Y}/\overline{Z}](\overline{Q}, \ \overline{U})}{\overline{Y} \ \prec: \ \overline{P} \vdash T_o \prec: [\overline{Y}/\overline{Z}]U_o }}{override(m, \ N, \ <\overline{Y}\triangleleft \overline{P}>\overline{T} \rightarrow T_o)}$ \\
    \\
    $\frac{mtype(m, \ N)\ =\ <\overline{Z}\triangleleft \overline{Q}> \ \overline{U} \rightarrow \  void \ implies \ \overline{P}, \ \overline{T} \ = \ [\overline{Y}/\overline{Z}](\overline{Q}, \  \overline{U})}{override(m, \ N, \ <\overline{Y}\triangleleft \overline{P}>\overline{T} \rightarrow void)}$ \\ \\
\hline 
 \end{tabular}
\caption{FGJP: Subtyping and well-formedness}
\end{table}Environment $\Gamma$ is a finite mapping from variables to types written x:T. Every type variable is bounded by a well defined type whether it be declared in class declaration or method declaration. A type environment, $\Delta$ is a mapping from type variable to its bound. \\
{\it Type Judgements:}
\begin{itemize}
 \item $\Delta \ \vdash$ S $\prec:$ T - Judgment that in the type environment $\Delta$ S is a subtype of T
 \item $\Delta\ \vdash$ T ok - Judgment that T is a well-formed type in the type environment $\Delta$
 \item $\Delta; \ \Gamma \ \vdash$ e : T - Judgment that expression e has a type T in the environment $\Gamma$ and type environment $\Delta$
\end{itemize}
 Similar to the earlier notation we denote a sequence of type judgments $\Delta \vdash$ T$_1$ ok, $\Delta \ \vdash $ T$_2$ ok... by $\Delta \ \vdash $ $\overline T$ ok. Similar notation is used for other judgments.\\
Table 6.3 summarizes the typing and well-formedness rules. \\
{\it Bound:} A type variable declared in a class declaration or method declaration is always bounded by a type, this is given by bound$_{\Delta}$(X). The bound of a non-variable type is itself.\\
{\it Subtyping:} Every type as well as void is a subtype of itself. Further, void is not a subtype of any other type. Also, no class can have void as its supertype. The subtype relation is transitive as shown by the rule S-TRANS. The rule S-CLASS denotes that replacing a type variable with another type variable for all its occurrences maintains the subtype relation.\\
{\it Well-formedness:} The type void is well-defined and according to the syntax, no variable can be of type void. It could occur only as the return type of a method. The base class Object is trivially well-formed and so is the class Process. Also, a type variable is well-formed if it belongs to the domain of type environment. If a class declaration is of the form class C$<\overline{X}\triangleleft\overline{N}>..$ then a type C$<\overline{T}>$ is well-formed if it respects the bounds of $\overline{N}$. $\Delta$ is the type environment where $\Delta$(X) gives the bound of the type variable X in dom($\Delta$). If the bounds of all the type variables in domain of $\Delta$ are well-formed then the environment $\Gamma$ is said to be well-formed. That is, if $\Delta \ \vdash$ $\Delta$(X) ok for all type variables in dom($\Delta$) then we say that $\Delta \ \vdash \ \Gamma $ ok. \\
The rule VD-DCAST says that if C extends D and if $\overline{X}$ are the only free variables in type variables of D and that X is bound in the declaration of C, then dcast(C, D) is valid. dcast(C, D) ensures that the result of the cast will be same at runtime, no matter whether we use the high-level type passing rule or the type erasure method. VD-TRANS shows that $dcast$ maintains transitive property.\\
In Java method overriding allows method in subclass to have a return type which is a subclass of the return type of method declared in supertype. If the return type is $void$ then according to rule S-VOIDSUB and S-VOIDSUP the return type in subclass also should be void.

\section{Typing}
%%TYPING 
\begin{table}
\resizebox{\textwidth}{!}{
  \begin{tabular}{|p{0.8\linewidth}r|}
    \hline\\
    {\bf Expression Typing} &\\
    $\Delta; \Gamma \ \vdash$ x :$\Gamma$(x) & GT-VAR\\ &\\
    $\frac{\Delta; \Gamma \ \vdash \ e_0:T_0 \hspace{1cm} fields(bound_\Delta(T_0) = \overline{T}\ (\overline{f})}{\Delta; \Gamma \ \vdash \ e_0.f_i\ :\ T_i}$ & GT-FIELD \\
    &\\
    $\frac{\splitfrac{\Delta;\Gamma \ \vdash \ e_0:T_0 \ \ mtype(m,\ bound_\Delta(T_0))\ =\ <\overline{Y}\triangleleft \overline{P}>\overline{U}\rightarrow \tau}{\Delta \vdash \ \overline{V}\ ok \ \ \Delta \vdash \ \overline{V} \prec:\ [\overline{V}/\overline{Y}]\overline{P} \ \ \Delta; \Gamma \ \vdash \ \overline{e}:\overline{S} \ \ \ \Delta \ \vdash \ \overline{S} \ \prec: \ [\overline{V}/\overline{Y}]\overline{U}}}{\Delta;\Gamma \ \vdash \ e_0.m<\overline{V}>(\overline{e})\ :\ [\overline{V}/\overline{Y}]\overline{U}}$ & GT-INVK \\ 
    &\\
    $\frac{\Delta \ \vdash \ N \ ok \ \ \ fields(N)=\overline{T} \ \overline{f} \ \ \Delta;\Gamma \ \vdash \ \overline{e}\ :\ \overline{S} \ \ \Delta \ \vdash \ \overline{S} \ \prec: \ \overline{T}}{\Delta;\Gamma \ \vdash \ new \ N(\overline{e})\ : \ N}$ & GT-NEW\\
    &\\
    $\frac{\Delta; \Gamma \ \vdash \ e_0\ :\ T_0 \ \ \Delta \ \vdash \ bound_{\Delta}(T_0) \ \prec: \ N}{\Delta; \Gamma \ \vdash \ (N)e_0 \ : \ N}$ & GT-UCAST \\
    &\\
    $\frac{\splitfrac{\Delta; \Gamma \ \vdash \ e_0\ :\ T_0 \ \ \Delta \ \vdash \ N \ ok \ \ \ \Delta \ \vdash \ N \ \prec: \ bound_{\Delta}(T_0)}{N = C<\overline{T}> \ \ \ bound_{\Delta}(T_0)=D<\overline{U}> \ \ \ dcast(C, D)}}{\Delta; \Gamma \ \vdash \ (N)e_0 \ : \ N}$ & GT-DCAST \\
    &\\
    $\frac{\splitfrac{\Delta; \Gamma \ \vdash \ e_0\ :\ T_0 \ \ \Delta \ \vdash \ N \ ok \ \ \ N = C<\overline{T}> \ \ \ bound_{\Delta}(T_0) = D<\overline{U}>}{C \unlhd \ D \ \ \ D\ \unlhd \ C  \ \ \ \ \ \ \ \ \ stupid \ warning}}{\Delta; \Gamma \ \vdash \ (N)e_0 \ : \ N}$ & GT-SCAST \\
    &\\
    \hline\\
    {\bf Method Typing} & \\
    $\frac{\splitfrac{\splitfrac{\Delta \ \vdash \overline{X}\ \prec: \ \overline{N}, \ \overline{Y} \prec: \ \overline{P} }{\Delta; \ \overline{x}\ : \ \overline{T}, \ this\ :\ C<\overline{X}> \ \vdash \ e_o:S \ \ \ \ \Delta \ \vdash \ S \ \prec: \ T}}{class \ C<\overline{X}\triangleleft \overline{N}>\triangleleft N \ \{...\} \ \ \ \ \ \ override(m,\ ,N, \ <\overline{Y} \triangleleft \overline{P}>\overline{T} \rightarrow T)}}{<\overline{Y}\triangleleft \overline{P}> \ T \ m(\overline{T} \ \overline{x})\ \{ \ return\ e_o; \ \} \ ok\ in \ C<\overline{X}\triangleleft \overline{N}>}$ & GT-METHOD\\
    &\\
    $\frac{\splitfrac{\splitfrac{\Delta; \ \overline{x}\ : \ \overline{T}, \ this\ :\ C<\overline{X}> \ \vdash \ e_o:void}{\Delta \ \vdash \overline{X}\ \prec: \ \overline{N}, \ \overline{Y} \prec: \ \overline{P}\ \ \ \ class \ C<\overline{X}\triangleleft \overline{N}>\triangleleft N \ \{...\}}}{ override(m,\ ,N, \ <\overline{Y} \triangleleft \overline{P}>\overline{T} \rightarrow void)}}{<\overline{Y}\triangleleft \overline{P}> \ void \ m(\overline{T} \ \overline{x})\ \{ \ return\ e_o; \ \} \ ok\ in \ C<\overline{X}\triangleleft \overline{N}>}$ & GT-METHOD-RET-VOID\\
    &\\
    $\frac{\splitfrac{\Delta \ \vdash \ e_1 \ ok \ \ \ \ \Delta \ \vdash \ e_2 \ ok}{\ isProcess(e_1) \ := \ true \ \ \ \ isProcess(e_2) \ := \ true}}{\splitfrac{\Delta; \Gamma \ \vdash \   e_1.run()\ \| \ e_2.run() \ : \ void}{\Delta; \Gamma \ \vdash \   e_1.run()\ \vee \ e_2.run() \ : \ void}}$ & GT-PROCESS-OP\\
    &\\
    $\frac{\splitfrac{\overline{X} \prec: \overline{N} \ \vdash \ \overline{N}, \ N, \ \overline{T} \ ok \ \ \ fields(N) = \overline{U} \ \overline{g} \ \ \ \ \overline{M} \ OK \ IN \ C<\overline{X}\triangleleft \overline{N}>}{K = C(\overline{U} \ \overline{g}, \ \overline{T} \ \overline{f}) \ \{ \ super(\overline{g}); \ this.\overline{f} = \overline{f} \ \}}}{class  \ C<\overline{X} \triangleleft \ \overline{N}> \triangleleft N \ \{\overline{T} \ \overline{f}; \ K \ \overline{M} \ \} \ OK}$ & GT-CLASS \\
    &\\
    \hline
\end{tabular}}
\caption{FGJP:Typing}
\end{table}
$\Gamma$(x) gives the type of a variable. Type of a field in a class or type variable is the type of field in its bound. 	\\

\section{Reduction}
In operational semantics a valid program is viewed as a sequence of computational steps. We use reduction semantics in order to understand the semantics of our program. Reduction semantics involves reducing or replacing current expression by a simpler or smaller expression until it cannot be further reduced to get a normal form. A programming language with properties of subject reduction and progress is type safe.\\
The FGJP reduction rules are formally written in Table 6.5. Field and method access will reduce to the corresponding field and method return value. The congruence rules are straight forward. In the last rule GR-PROCESS, if e$_1$ and $e_2$ are processes then the expression after applying the operator choice or parallel will reduce to the corresponding base value denoted by choice(e$_1$, e$_2$) and parallel(e$_1$, e$_2$).
\begin{table}
 \begin{tabular}{|p{0.8\linewidth}r|}
    \hline\\
    {\bf Computation:} & \\
    $\frac{fields(N) = \overline{T} \ \overline{f}}{(new\ N(\overline{e})).f_i \rightarrow e_i}$ & GR-FIELD \\
    & \\
    $\frac{mbody(m<\overline{V}>, \ N)\ = \ \overline{x}.e_o}{(new\  N(\overline{e})).m<\overline{V}>(\overline{d}) \rightarrow [\overline{d}/\overline{x},\ new\  N(\overline{e})/this]e_o}$ & GR-INVK\\
    &\\
    &\\
    {\bf Congruence:} & \\
    $\frac{e_o \rightarrow e_o'}{e_o.f \rightarrow \ e_o'.f}$ & GRC-FIELD\\
    &\\
    $\frac{e_o \rightarrow e_o'}{e_o.m<\overline{T}>(\overline{e} \rightarrow e_o'.m<\overline{T}>(\overline{e}))}$ & GRC-INV-RECV\\
    &\\
    $\frac{e_i \rightarrow \ e_i'}{e_o.m<\overline{T}>(....,\ e_i, ....)\rightarrow \ e_o.m<\overline{T}>(...., e_i',....)}$ & GRC-INV-ARG \\
    &\\
    $\frac{e_i \rightarrow \ e_i'}{new \ N(....,\ e_i, ....)\rightarrow \ new \ N(...., e_i',....)}$ & GRC-NEW-ARG \\
    &\\
    $\frac{e_o \rightarrow \ e_o'}{(N)e_o \rightarrow \ (N)e_o'}$ & GRC-CAST \\
    &\\
    {\bf Running process:} & \\
    $\frac{isProcess(e_1) = true \ \ \ isProcess(e_2) = true}{\splitfrac{e_1.run() \ \vee \ e_2.run()\rightarrow \ choose(e_1, e_2)}{e_1.run() \ \| \ e_2.run()\rightarrow \ parallel(e_1, e_2)}}$ & GR-PROCESS \\
    &\\
    \hline
 \end{tabular}
\caption{FGJP:Reduction}
\end{table}
{\bf Theorem 6.6.1: (Subject Reduction)}: If $\Delta; \Gamma \ \vdash \ e\ : \ \tau$ and $e\rightarrow^* \ e'$ then $\Delta; \Gamma \ \vdash \ e' \ : \ \tau'$, for some $\tau'$ such that $\Delta \ \vdash \ \tau \ \prec:\ \tau'$.\\
{\bf Proof:} See Appendix A.1. $\Box$\\
{\bf Theorem 6.6.2: (Progress)}: If e is a well-typed expression, then\\
\begin{itemize}
 \item If e includes $new \ N_o(\overline{e}).f$ as a subexpression then $fields(N_o)\ = \ \overline{T} \ \overline{f} $ and $f \ \in \ \overline{f}$ for some $\overline{T}$ and $\overline{f}$.
 \item If e includes $new \ N_o(\overline{e}).m<\overline{V}>(\overline{d})$ as a subexpression, then $mbody(m<\overline{V}>, N_o) = \overline{x}.e_o$ and \#(x) = \#(d).
\end{itemize}
{\bf Proof:} Case 1: By well-typedness of the subexpression, $fields(N_o)$ is well defined and f appears in it. \\
Case 2: Similarly for method call, a method with $mbody(m<\overline{V}>, N_o) = \overline{x}.e_o$ and \#(x) = \#(d) from the fact that $mtype(m, N_o) \ = \ \overline{N}\rightarrow \ \tau$ where \#($\overline{N}$) = \#($\overline{x}$) $\Box$ \\ \\ \\
To state type soundness formally, consider the following definition of values, or normal form of expression, given by the following syntax : 
\begin{center}
 v := new C($\overline{V}$)\\
 v := choose($e_1$, $e_2$)\\
 v := parallel($e_1$, $e_2$)
\end{center}
{\bf Theorem 6.6.3: (FGJP Type soundness)}: If $\phi; \phi \ \vdash \ e \ : \ \tau \ and \ e \rightarrow^* \ e'$ with $e'$ a normal
 form, then $e'$ is either a value with $\phi; \phi \ \vdash \ v \ : \ \tau' \ and \ \tau' \ \prec: \ \tau$, or an expression
 containing $(\tau')new \ \tau(\overline{e}) \ where \ \tau \ \prec: \ \tau'$ or an expression containing choose($e_1$, $e_2$) or an expression containing parallel($e_1$, $e_2$)\\
{\bf Proof:} Immediate from Theorems 6.6.1 and 6.6.2 $\Box$ \\ 

